eajs.5.jani:model: info: eajs.5 is an MDP model and will be simulated as an MDP.
eajs.5.jani:variables[11]: info: Expanding variable "loc_1" into 3 locations in automaton "Process_1".
eajs.5.jani:variables[15]: info: Expanding variable "loc_2" into 3 locations in automaton "Process_2".
eajs.5.jani:variables[17]: info: Expanding variable "user_1" into 6 locations in automaton "Resources".
eajs.5.jani:variables[19]: info: Expanding variable "loc_3" into 3 locations in automaton "Process_3".
eajs.5.jani:variables[20]: info: Expanding variable "loc_5" into 3 locations in automaton "Process_5".
eajs.5.jani:variables[23]: info: Expanding variable "loc_4" into 3 locations in automaton "Process_4".
eajs.5.jani: info: Using default value of 0.95 for the confidence parameter.
eajs.5.jani: warning: Using the Chow-Robbins method for relative-width sequential confidence intervals, which guarantees the requested confidence only asymptotically for decreasing width.
Peak memory usage: 61 MB
Analysis results for eajs.5.jani
Experiment energy_capacity=250, B=11
Status: Finished
Simulation time: 599.5 s
+ Property Property "ExpUtil"
Estimated max. value: 3.37913669064748
Max. confidence interval: [3.311589069684935, 3.446684311610025]
Runs used (best scheduler): 1390
Total runs used: 8578400
Schedulers sampled: 8000
Best scheduler: 1823521485
Run type: MDP
Status: Finished
+ Max. sample data
Mean: 3.37913669064748
Variance: 1.650968296636989
Skewness: 0.3228499023677422
Kurtosis: 2.741629925379005
+ Error bounds
Scheduler sampling: The result is a lower bound for the true max. value.
Statement: CI: 100(1 - α)% of intervals contain true value (CLT assumption)
α: 0.050000000000000044